(declare-const v1 Bool)
(declare-const v3 Bool)
(declare-const v6 Bool)
(declare-const v8 Bool)
(declare-const _4-0 (_ BitVec 4))
(declare-const _8-3 (_ BitVec 8))
(declare-const _1-0 (_ BitVec 1))
(declare-const _15-0 (_ BitVec 15))
(assert (or v6 v6 (= (_ bv147 8) (_ bv147 8) (_ bv147 8)) (and (bvule _8-3 #b01010101) v1 v8 (and v8 v6 (xor v8 v1 v8) (distinct #b01010101 (_ bv147 8)) (distinct #b01010101 (_ bv147 8)) (bvsgt #b0111101 (bvnor #b0111101 #b0111101))) v6) (and (bvule _8-3 #b01010101) v1 v8 (and v8 v6 (xor v5 v8 v1 v8) (distinct #b01010101 (_ bv147 8)) (distinct #b01010101 (_ bv147 8)) (bvsgt #b0111101 (bvnor #b0111101 #b0111101))) v6)))
(assert (or (bvule _8-3 #b01010101)))
(check-sat)
